; REQUIRES: cocoa
; EXPECT: unsat
; COMMAND-LINE: --ff-solver split
; COMMAND-LINE: --ff-solver gb
(set-info :smt-lib-version 2.6)
(set-logic QF_FF)

(declare-const b Bool)
(declare-const a Bool)
(declare-const c Bool)
(declare-const return_n0 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const mul_n7 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const mul_n8 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const mul_n5 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const b_n1 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const mul_n6 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const a_n2 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const mul_n4 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const c_n3 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(assert
	(not (=> (and (and (= b_n1 (ite b #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= c_n3 (ite c #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= a_n2 (ite a #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513))) (and (= (ff.mul b_n1 (ff.add b_n1 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513)) #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513) (= (ff.mul a_n2 (ff.add a_n2 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513)) #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513) (= (ff.mul c_n3 (ff.add c_n3 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513)) #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513) (= (ff.mul a_n2 (ff.add (ff.mul a_n2 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) c_n3)) mul_n4) (= (ff.mul (ff.add mul_n4 a_n2) (ff.add (ff.mul b_n1 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) mul_n5) (= (ff.mul mul_n5 (ff.add (ff.mul mul_n4 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) (ff.mul a_n2 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) mul_n6) (= (ff.mul mul_n6 (ff.add (ff.mul b_n1 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) mul_n7) (= (ff.mul (ff.add (ff.mul mul_n5 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513) (ff.add (ff.mul mul_n7 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) mul_n8) (= (ff.mul mul_n8 (ff.add (ff.mul mul_n7 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) return_n0))) (and (or (= #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 return_n0) (= #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513 return_n0)) (= (= #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 return_n0) (and (=> (ite a c a) b) (or (=> (ite a c a) b) (ite a c a) b) (or (=> (ite a c a) b) (ite a c a) b))))))
)
(check-sat)
